1. Field of Invention
The present invention relates to the field of verifying two or more designs of circuits to determine if the devices and interconnections found in one design appear in the same way in the other designs.
2. Prior Art
When designing an electric circuit it is customary to start with an abstract logic design called a schematic. This will identify the logic components and interconnects necessary to provide the desired functionality. An example of this can be found in FIG. 1a, where five logic components, 1, 2, 3, 4, 5, two input ports, a, b, one output port out, power supply VDD and ground connection VSS are shown. The interconnects between the components and between the components and the ports are represented with the wires in FIG. 1a. To avoid too much clutter the power supply and ground connections are symbolized with labels on top of short wire segments. Components 1, 2 in FIG. 1a represent fundamental logic devices called CMOS pfet and nfet transistors. The schematic of components 3 and 5, also known as a nor-gate, is shown in FIG. 1b. FIG. 1c shows the schematic of component 2, commonly referred to as a nand-gate. A component that is not a fundamental device but instead contains such devices or other components, see FIGS. 1b,c, is referred to as a subcircuit. The schematic in FIG. 1a is known as the top-level design, since it is not a subcircuit of any of the other schematics in FIGS. 1b,c. Modern circuit design has many other fundamental devices available, such as bipolar transistors, inductors, capacitors, resistors among others. The basic CMOS devices described here is for simplicity and illustrative purposes only and the discussion shall in no way be interpreted as limited to a particular set of devices.
After the logic design is finished it is translated into a layout, which describes layer by layer how the design is to be built on a piece of silicon or printed circuit board or other such materials. FIG. 2 shows an example of a layout corresponding to the schematic in FIG. 1a. The layout consists of three subcircuits and CMOS nfet and pfet transistors corresponding to components 1-5 in FIG. 1a. The interconnections between the components can also be seen in FIG. 2.
Both the schematic and layout can furthermore be described by what is called a netlist. It is a list of subcircuits and their constituting components. Interconnections, called nets or nodes, are symbolized with identical names appearing at the appropriate ports of the connected components. FIG. 5 shows an example of a netlist. It contains three separate subcircuits, “Adder”, “nor”, and “nand”, where “Adder” is the netlist of the schematic in FIG. 1a. The “nor” and “nand” netlists correspond to the schematics in FIGS. 1 b,c. In the “Adder” subcircuit there are copies, or instantiations, of the “nor” and “nand” subcircuits. As FIG. 5 illustrates, the netlist typically consists of many separate subcircuits, where each subcircuit is represented by a name and a list of input and output ports. These ports represent the connections between the inside of the subcircuit and the outside environment. A subcircuit furthermore consists of a list of electronic devices such as transistors, resistors, capacitors and other such fundamental devices and their interconnections. A subcircuit can also consist of other subcircuits (i.e. instantiations of other subcircuits), see “Adder” in FIG. 5. Thereby one can create a hierarchical structure where the lowest level subcircuits consist of fundamental devices only, see “nor” and “nand” in FIG. 5. The top-level hierarchy is the highest hierarchy level of interest.
The layout netlist and schematic netlist now needs to be verified for logical equivalence, so that each component in the schematic netlist has a corresponding one in the layout with the same interconnects to the other components. This verification procedure is what we are concerned with in this invention. There are other situations where a similar logical netlist verification is necessary. It is, for example, often useful to copy a design made in one technology, say 0.13 um CMOS to another technology such as 0.09 um CMOS. It is then again necessary to verify that the two schematic representations are logically equivalent.
To solve the problem of comparing different netlists, inventors have over the years followed two different paths. Initially all netlists were flattened, a process in which all subcircuit instantiations are removed and replaced by their fundamental device contents. There are many published and otherwise known ways to solve this problem commonly referred to as graph isomorphic methods, see for example articles by C. Ebeling “Gemini II, A second generation layout verification program”, IEEE ICCAD-88, Digest of Technical Papers. pp. 322-325, Nov. 7-10 1988 and R. L. Spickelmier and A. R. Newton, “WOMBAT a new netlist comparison program” IEEE Int. Conference on CAD, pages 170-171, September 1983. As the design complexity grew it became necessary to take advantage of the hierarchical description of the circuit and several methods appeared.
The invention by Razdan, U.S. Pat. No. 5,463,561 to Razdan entitled “High Capacity netlist comparison”, concerns designs consisting of mosfet devices only and describes a method of simplifying the circuit and thereby reducing the complexity when verifying logical equivalence.
The method of Okuzawa et al, U.S. Pat. No. 5,243,538 to Okuzawa et al. entitled “Comparison and verification for logic circuits and verification thereof”, is of great use when verifying complex digital designs and is not very suitable for more general designs.
Ho et al., U.S. Pat. No. 6,009,251 entitled “Method and system for layout verification of an integrated circuit design with reusable sub designs”, describes a method where if you are using the same design multiple times there is no need to reverify its logical equivalence again and again. Unfortunately, there is always a need to reverify a design because of the high risk of database corruption and in practice the method is not used much.
Lipton et al's invention, U.S. Pat. No. 6,505,323 entitled “Methods apparatus and computer programs products that perform layout versus schematic comparison of integrated circuit memory devices using bit cell detection and depth first searching techniques”, is concerned with the special case where there is a lot of redundancy in the designs, such as memory circuits, and how one can arrange the analysis in such a way as to reduce the time spent resolving such redundancies.
The invention by Batra, U.S. Pat. No. 5,249,133 entitled “Methods for the hierarchical comparison of schematic and layout of electrical components”, is more general in nature and of more interest to the present discussion. It is also a methodology used by many commercial tools. The basic idea in Batra's method is to order all subcircuits, in a given design, in hierarchical order and start the verification at the lowest hierarchical level and work upwards in the hierarchy until reaching the top-level. This ordering is necessary since it is assumed nothing is known about the subcircuits and their ports. For each subcircuit one has to find a one to one correspondence between each subcircuit port in the netlists. Once this is known one can use this information for all instantiations of this subcircuit and the verification can proceed to the next level in the hierarchy. There are several disadvantages with this approach:                (a) The subcircuits need to be ordered from the lowest to the highest hierarchy level.        (b) The verification procedure is necessarily also from the lowest hierarchy to the top-level hierarchy.        (c) If one is working on the top-level layout design and wants to have it verified one has to wait for all lower level subcircuits to be verified before one can get the desired result.        (d) One has to keep track of the subcircuit port map from netlist to netlist. This cost both memory space and computational overhead.        
The invention by Riepe et al., U.S. Pat. No. 7,103,863 entitled “Representing the design of a sub-module in a hierarchical integrated circuit design and analysis system”, concerns itself with other aspects of the layout verification process such as timing verification of the integrated circuit. The basic idea is that one can remove from the circuit such part that do not contribute to the timing delay thus achieving a sometimes significant increase in verification speed. The invention cannot be used for verifying logical equivalence, the problem the present invention solves.
The invention by Aik, Eric Teh Gim, U.S. Pat. No. 7,162,703 entitled “Electrical design rule checking expert traverser system”, describes an invention for checking design rules associated with nodes or a plurality of nodes in particular netlist. This can help in catching design “errors”, such as floating gates, early in the design phase. It thus solves a different problem than the present invention.
The invention by Dupenloup, Guy, U.S. Pat. No. 6,289,491 entitled “Netlist analysis tool by degree of conformity”, describes an invention that analyzes a particular netlist, its hardware elements, characteristics and interconnections and how this conforms to predetermined properties. For example, it can discover if a netlist generated from an RTL description supports the appropriate clocking scheme. It thus concerns itself with characteristics internal to a particular netlist and not logical equivalence of two different netlists.
The invention by Beausang et al., U.S. Pat. No. 6,106,568 entitled “Hierarchical scan architecture for design for test applications” discusses a method for architecting design for test circuitry. In modern integrated circuits, in particular ones that are dominated by digital circuitry with tens of millions of digital gates, methods for testing functionality of individual elements such as register blocks, is very important. Beausang describes a method that can among other things detect design-for-test structures already in place in a particular subcircuit. It thus is concerned with characteristics internal to a particular netlist and not the logical equivalence of two different netlists.